Nuprl Lemma : es-is-prior-interface
11,40
postcript
pdf
es
:ES,
X
:AbsInterface(Top),
e
:E. (
(
e
prior(
X
)))
(
e'
:E. ((
e'
<loc
e
) & (
(
e'
X
))))
latex
Definitions
x
.
A
(
x
)
,
e
X
,
ES
,
AbsInterface(
A
)
,
Top
,
E
,
P
Q
,
b
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
x
:
A
B
(
x
)
,
P
Q
Lemmas
es-local-pred-property
,
es-E
wf
,
es-interface
wf
,
top
wf
,
event
system
wf
origin
es:ES, X:AbsInterface(Top), e:E. (
(e 
prior(X))) 
(
e':E. ((e' <loc e) & ((e' X)))) es:ES, X:AbsInterface(Top), e:E. ((e prior(X))) (e':E. ((e' <loc e) & ((e' X)))) 
x.A(x) X Qbx:A. B(x)
B(x)
B(x) Q